Require Import AutoSep.

Definition swapS := SPEC("x", "y") reserving 2
  Ex v, Ex w,
  PRE[V] V "x" =*> v * V "y" =*> w
  POST[_] V "x" =*> w * V "y" =*> v.

Definition swap := bmodule "swap" {{
  bfunction "swap"("x", "y", "v", "w") [swapS]
    "v" <-* "x";;
    "w" <-* "y";;
    "x" *<- "w";;
    "y" *<- "v";;
    Return 0
  end
}}.

Theorem swapOk : moduleOk swap.
Proof.
  vcgen; sep_auto.
Qed.

Definition sillyS := SPEC("p", "q") reserving 5
  PRE[V] V "p" =?> 1 * V "q" =?> 1
  POST[R] [| R = 3 |] * V "p" =?> 1 * V "q" =?> 1.

Definition sillyM := bimport [[ "swap"!"swap" @ [swapS] ]]
bmodule "silly" {{
    bfunction "main"("p", "q") [sillyS]
      "p" *<- 3;;
      "q" *<- 8;;

      Call "swap"!"swap"("p", "q")
      [ Ex v,
        PRE[V] V "q" =*> v
        POST[R] [| R = v |] * V "q" =*> v ];;

      "q" <-* "q";;
      Return "q"
    end
  }}.

Theorem sillyMOk : moduleOk sillyM.
Proof.
  vcgen.
  Focus 5.
  post.
  evaluate auto_ext.
  descend.
  step auto_ext.
  step auto_ext.
  step auto_ext.
  descend; step auto_ext.
  step auto_ext.
  step auto_ext.
  descend; step auto_ext.
  step auto_ext.
  step auto_ext.
  words.
  step auto_ext.
  Abort.

Hint Extern 1 (@eq W _ _) => words.

Theorem sillyMOk : moduleOk sillyM.
Proof.
  vcgen; (sep_auto; auto).
Qed.